1. Field of the Present Invention
The present invention is in the field of integrated circuit design and, more particularly, systems and methods for design verification.
2. History of Related Art
In the field of integrated circuit design, formal verification refers to the process of rigorously proving that a design satisfies its specification. Typically, the specification of a verification problem includes a netlist-based representation of the design and a set of expected values for specified nets. As an example, a verification problem may include determining whether a state exists in which a CHECKSTOP signal is asserted, where an asserted CHECKSTOP signal indicates a fault. Using formal verification, one either finds a counterexample trace depicting a sequence of values of the nets over time, similar to a simulation trace, that leads to an assertion of the CHECKSTOP signal or proves that no such trace exists.
Formal verification is often performed using state space search algorithms. Such algorithms include unbounded and bounded exhaustive searches. Bounded exhaustive searches try to find an assertion of CHECKSTOP that can occur within N time steps from an initial state of the design. Unbounded exhaustive algorithms increase N until no states are encountered that have not already been encountered for smaller values of N (a condition termed “fixed-point”). If no path from an initial state to a violating state (a state in which CHECKSTOP is asserted) is encountered before fixed-point is reached, then correctness can be inferred.
The number of verification cycles required to perform an exhaustive state space search increases exponentially with the number of state holding elements or registers. This exponential relationship makes it highly desirable to reduce the number of elements in a design model. One well-known technique for reducing or simplifying a model is to eliminate redundancy. Redundancy refers to elements of the design model that exhibit identical behavior. If redundant elements can be established, the model can be simplified by replacing multiple elements with a single element. One type of redundancy removal is referred to as sequential redundancy removal because it operates on a sequential model of the design.
Conventional sequential redundancy removal begins by proposing a set of elements thought to be equivalent. Thereafter, conventional sequential redundancy removal attempts to prove formally that the proposed elements are equivalent. This proof is traditionally attempted using a fixed-point iteration, such as enumerating all reachable states of the design—which tends to be prohibitively expensive—or by using an approximate approach such as induction.
In common inductive methods, the design is effectively initialized into any arbitrary state where all of the proposed equivalent elements have the same value (either be 0 or 1). Inductive methods then attempt to demonstrate that each of the proposed elements remain equivalent one time step from the initial state. More generally, k-step induction includes placing the design into any arbitrary initial state, with the constraint that the suspected equivalent elements are equivalent for the initial states and all states transitioned to within k−1 time steps, and then verifying that the set of states transitioned to in k steps also satisfy the suspected equivalence relation. Skilled practitioners will appreciate that induction algorithms are resource intensive. Moreover, induction algorithms are “weak” in the sense that they cannot differentiate between assertions of a target associated with an unreachable state and other assertions of the target.
It would be desirable to implement a sequential redundancy removal process that is at least as robust as existing methodologies, but does not required the resources associated with induction and reachability algorithms. Moreover, conventional verification algorithms do not attempt to make good use of suspected redundancy until equivalence is formally proven. It would be desirable to implement a verification method that was able to obtain meaningful verification information using suspected, but unproven, redundancy.